T:Type, L:(T List). (x:T. (x  L))  ((L = [])) 

latex

ProofTree

Definitions

Type, t  T, s = t, type List, [], , x:AB(x), x:A. B(x), A, x:A  B(x), x:A. B(x), Void, P  Q, False, , (x  l), P  Q, a < b, P & Q, P  Q, tl(l), n - m, if a<b then c else d, i <z j, b, i z j, case b of inl(x) => s(x) | inr(y) => t(y), if b then t else f fi , nth_tl(n;as), hd(l), l[i], n+m, rec-case(a) of [] => s | x::y => z.t(x;y;z), x.A(x), Y, ||as||, A  B, , {x:A| B(x)} , , {T}, A List, [car / cdr]

Lemmas

member exists, nil member, iff wf, false wf, rev implies wf, l member wf, not wf